Computational verification of C protocol implementations by symbolic execution

ABSTRACT

We verify cryptographic protocols coded in C for correspondence properties with respect to the computational model of cryptography. The first step uses symbolic execution to extract a process calculus model from a C implementation of the protocol. The new contribution is the second step in which we translate the extracted model to a CryptoVerif protocol description, such that successful verification with CryptoVerif implies the security of the original C implementation. We implement our method and apply it to verify several protocols out of reach of previous work in the symbolic model (using ProVerif), either due to the use of XOR and Diffie-Hellman commitments, or due to the lack of an appropriate computational soundness result. We analyse only a single execution path, so our tool is limited to code following a fixed protocol narration. This is the first security analysis of C code to target a verifier for the computational model. We successfully verify over 3000 LOC. One example (about 1000 LOC) is independently written and currently in testing phase for industrial deployment; during its analysis we uncovered a vulnerability now fixed by its author.

References

1. M. Abadi, B. Blanchet, and H. Comon-Lundh. Models and proofs of protocol security: A progress report. In A. Bouajjani and O. Maler, editors, CAV, volume 5643 of Lecture Notes in Computer Science, pages 35--49. Springer, 2009.
2. M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptology, 15(2):103--127, 2002.
3. M. Abe and V. D. Gligor, editors. Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, ASIACCS 2008, Tokyo, Japan, March 18--20, 2008. ACM, 2008.
4. M. Aizatulin, F. Dupressoir, A. D. Gordon, and J. Jürjens. Verifying cryptographic code in C: Some experience and the Csec challenge. In Formal Aspects of Security and Trust (FAST 2011), Lecture Notes in Computer Science. Springer, 2011.
5. M. Aizatulin, A. D. Gordon, and J. Jürjens. Extracting and verifying cryptographic models from C protocol code by symbolic execution. In 18th ACM Conference on Computer and Communications Security (CCS 2011), 2011. Full version available at http://arxiv.org/abs/1107.1017.
6. M. Aizatulin, A. D. Gordon, and J. Jürjens. Computational verification of C protocol implementations by symbolic execution. Technical Report MSR-TR-2012-80, Microsoft Research, 2012.
7. M. Backes, D. Hofheinz, and D. Unruh. CoSP: A general framework for computational soundness proofs. In ACM Conference on Computer and Communications Security, pages 66--78, 2009. Preprint on IACR ePrint 2009/080.
8. M. Backes, M. Maffei, and D. Unruh. Computationally sound verification of source code. In CCS, 2010.
9. M. Barbosa, J. Pinto, J. Filliâtre, and B. Vieira. A deductive verification platform for cryptographic software. In Proceedings of the Fourth International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), volume 33 of Electronic Communications of the EASST. EASST, 2010.
10. G. Barthe, B. Grégoire, S. Heraud, and S. Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Advances in Cryptology -- CRYPTO 2011, Lecture Notes in Computer Science. Springer, 2011.
11. J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. In CSF '08: Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, pages 17--32. IEEE Computer Society, 2008.
12. K. Bhargavan, R. Corin, C. Fournet, and E. Zalinescu. Automated computational verification for cryptographic protocol implementations. Unpublished draft, Oct. 2009.
13. K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu. Cryptographically verified implementations for TLS. In CCS '08: Proceedings of the 15th ACM conference on Computer and communications security, pages 459--468, Alexandria, VA, Oct. 2008. ACM.
14. K. Bhargavan, C. Fournet, and A. D. Gordon. Modular verification of security protocol code by typing. In ACM Symposium on Principles of Programming Languages (POPL'10), pages 445--456, 2010.
15. K. Bhargavan, C. Fournet, A. D. Gordon, and N. Swamy. Verified implementations of the information card federated identity-management protocol. In Abe and Gligor {3}, pages 123--135.
16. K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse. Verified interoperable implementations of security protocols. In CSFW '06: Proceedings of the 19th IEEE workshop on Computer Security Foundations, pages 139--152. IEEE Computer Society, 2006.
17. B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In CSFW, pages 82--96. IEEE Computer Society, 2001.
18. B. Blanchet. Computationally sound mechanized proofs of correspondence assertions. In 20th IEEE Computer Security Foundations Symposium (CSF'07), pages 97--111, Venice, Italy, July 2007. IEEE.
19. B. Blanchet. A computationally sound mechanized prover for security protocols. IEEE Transactions on Dependable and Secure Computing, 5(4):193--207, Oct.-Dec. 2008.
20. B. Blanchet, A. D. Jaggard, A. Scedrov, and J.-K. Tsay. Computationally sound mechanized proofs for basic and public-key kerberos. In Abe and GligorciteDBLP:conf/ccs/2008asia, pages 87--99.
21. C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), San Diego, CA, Dec. 2008.
22. D. Cadé and B. Blanchet. From computationally-proved protocol specifications to implementations. In International Conference on Availability, Reliability and Security (ARES 2012), 2012.
23. S. Chaki and A. Datta. ASPIER: An automated framework for verifying security protocol implementations. In Computer Security Foundations Workshop, pages 172--185, 2009.
24. R. Corin and F. A. Manzano. Efficient symbolic execution for analysing cryptographic protocol implementations. In International Symposium on Engineering Secure Software and Systems (ESSOS'11), LNCS. Springer, 2011.
25. V. Cortier, S. Kremer, and B. Warinschi. A survey of symbolic methods in computational analysis of cryptographic systems. J. Autom. Reasoning, 46(3--4):225--259, 2011.
26. D. Dolev and A. Yao. On the Security of Public-Key Protocols. IEEE Transactions on Information Theory, 29(2):198--208, 1983.
27. F. Dupressoir, A. D. Gordon, J. Jürjens, and D. A. Naumann. Guiding a general-purpose C verifier to prove cryptographic protocols. In 24th IEEE Computer Security Foundations Symposium, 2011.
28. B. Dutertre and L. D. Moura. The Yices SMT Solver. Technical report, Computer Science Laboratory, SRI International, 2006.
29. C. Fournet, K. Bhargavan, and A. D. Gordon. Cryptographic verification by typing for a sample protocol implementation. In Foundations of Security and Design VI (FOSAD 2010), Lecture Notes in Computer Science. Springer, 2011. To appear.
30. C. Fournet, M. Kohlweiss, and P.-Y. Strub. Modular code-based cryptographic verification. In 18th ACM Conference on Computer and Communications Security (CCS 2011), 2011.
31. http://frama-c.cea.fr/, 2009.
32. P. Godefroid and S. Khurshid. Exploring very large state spaces using genetic algorithms. In Tools and Algorithms for Construction and Analysis of Systems (TACAS'02), volume 2280, pages 266--280. Springer, 2002.
33. P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In Programming Language Design and Implementation (PLDI'05), pages 213--223. ACM, 2005.
34. S. Goldwasser and S. Micali. Probabilistic encryption. Journal of Computer and System Science, 28(2):270--299, 1984.
35. A. D. Gordon. Provable implementations of security protocols. In LICS, pages 345--346, 2006.
36. J. Goubault-Larrecq and F. Parrennes. Cryptographic protocol analysis on real C code. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of Lecture Notes in Computer Science, pages 363--379. Springer, 2005.
37. P. Gupta and V. Shmatikov. Towards computationally sound symbolic analysis of key exchange protocols. In V. Atluri, P. Samarati, R. Küsters, and J. C. Mitchell, editors, FMSE, pages 23--32. ACM, 2005.
38. C. Hritcu. Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD thesis, Department of Computer Science, Saarland University, 2011.
39. A. Jeffrey and R. Ley-Wild. Dynamic model checking of C cryptographic protocol implementations. In Proceedings of Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, 2006.
40. J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385--394, 1976.
41. R. Küsters and T. Truderung. Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. Journal of Automated Reasoning, 46(3):325--352, 2011.
42. R. Küsters, T. Truderung, and J. Graf. A Framework for the Cryptographic Verification of Java-like Programs. In IEEE Computer Security Foundations Symposium, CSF 2012. IEEE Computer Society, 2012.
43. R. Küsters and M. Tuengerthal. Computational soundness for key exchange protocols with symmetric encryption. In E. Al-Shaer, S. Jha, and A. D. Keromytis, editors, ACM Conference on Computer and Communications Security, pages 91--100. ACM, 2009.
44. P. Lincoln, J. C. Mitchell, M. Mitchell, and A. Scedrov. Probabilistic polynomial-time equivalence and security analysis. In J. M. Wing, J. Woodcock, and J. Davies, editors, World Congress on Formal Methods, volume 1708 of Lecture Notes in Computer Science, pages 776--793. Springer, 1999.
45. G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In Proceedings of the 11th International Conference on Compiler Construction, CC '02, pages 213--228, London, UK, 2002. Springer-Verlag.
46. PolarSSL. http://polarssl.org.
47. N. Polikarpova and M. Moskal. Verifying implementations of security protocols by refinement. In Verified Software: Theories, Tools and Experiments (VSTTE 2012), volume 7152 of Lecture Notes in Computer Science, pages 50--65. Springer, 2012.
48. Project EVA. Security protocols open repository, 2007. http://www.lsv.ens-cachan.fr/spore/.
49. A. Rial and G. Danezis. Privacy-friendly smart metering. Technical Report MSR-TR-2010-150, Microsoft Research, 2010.
50. O. Udrea, C. Lumezanu, and J. S. Foster. Rule-Based static analysis of network protocol implementations. IN PROCEEDINGS OF THE 15TH USENIX SECURITY SYMPOSIUM, pages 193--208, 2006.
51. D. Unruh. The impossibility of computationally sound XOR, July 2010. Preprint on IACR ePrint 2010/389.

Index Terms

• Networks

  • Network protocols

    • Protocol correctness

      • Protocol testing and verification